(agda2-verbose "Checking D. ")
